\section{Implementation}
We have written the first version of a tool which generates formulae for
completeness and disjointness of Scala pattern matching expressions. As of now,
we don't work on the abstract syntax tree representation of the Scala compiler
itself yet, but instead on an intermediate representation of our design. Thus
the examples we worked on had to be manually encoded. Similarly, the class
hierarchy also has to be specified explicitely. We believe we used the right
level of abstraction for our intermediate form, and writing a converter from
the \texttt{scalac} AST to it should be relatively simple. However, this is
left as future work.

The formulae we generate are sent to \texttt{formDecider}, a component of the
Jahob system \cite{Jahob}, which automagically determines whether they're valid
or not. In the current implementation, all we do is displaying a message with
the result. Once the integration with \texttt{scalac} is complete, we will generate
appropriate warning messages for the end user.

We are quite satisfied with the range of pattern matching expressions we can
verify. Although support for primitive types is still scarce --~only integers
are already supported~-- and guards are still treated quite conservatively, we
have managed to properly verify numerous non trivial examples, which we believe
are representative of what is expected to be encountered in Scala programs.
